YES 12.789 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: Ratio Int  ->  [(Ratio Int,a)]  ->  Maybe a) :: Ratio Int  ->  [(Ratio Int,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: Ratio Int  ->  [(Ratio Int,a)]  ->  Maybe a) :: Ratio Int  ->  [(Ratio Int,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup0 k x y xys True = lookup k xys

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 ww wx = lookup2 ww wx



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: Ratio Int  ->  [(Ratio Int,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
QDP
              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup17(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup123(wy682, wy683, wy684, wy685, cd) → new_lookup(:%(Neg(Zero), Pos(Succ(wy682))), wy685, cd)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, Succ(wy7580), Succ(wy7590), cf) → new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, wy7580, wy7590, cf)
new_lookup16(wy642, wy643, wy644, wy645, Succ(wy6460), Zero, be) → new_lookup(:%(Pos(Zero), Pos(Succ(wy642))), wy645, be)
new_lookup(:%(Pos(Zero), wy31), :(@2(:%(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), wy31), wy41, bb)
new_lookup1(wy207, Pos(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, ba)
new_lookup19(wy668, wy669, wy670, wy671, Zero, Succ(wy6730), cb) → new_lookup121(wy668, wy669, wy670, wy671, cb)
new_lookup1(wy207, Neg(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, ba)
new_lookup(:%(Neg(Succ(wy3000)), wy31), :(@2(:%(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup18(wy3000, wy31, wy400000, wy4001, wy401, wy41, wy3000, wy400000, bb)
new_lookup15(wy635, wy636, wy637, wy638, Succ(wy6390), Zero, bd) → new_lookup(:%(Pos(Zero), Neg(Succ(wy635))), wy638, bd)
new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, Succ(wy7760), Succ(wy7770), bh) → new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, wy7760, wy7770, bh)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup117(wy264, wy265, wy266, wy267, wy268, wy269, bg) → new_lookup(:%(Neg(Succ(wy264)), wy265), wy269, bg)
new_lookup18(wy264, Neg(Succ(wy26500)), wy266, Neg(Zero), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Succ(wy26500)), wy266, Neg(Zero), wy268, wy269, bg)
new_lookup(:%(Neg(Succ(wy3000)), wy31), :(@2(:%(Neg(Zero), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Succ(wy3000)), wy31), wy41, bb)
new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, Zero, Succ(wy2140), ba) → new_lookup10(wy207, wy208, wy209, wy210, wy211, wy212, ba)
new_lookup18(wy264, Neg(Succ(wy26500)), wy266, Neg(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup120(wy264, wy26500, wy266, wy26700, wy268, wy269, wy26500, wy26700, bg)
new_lookup1(wy207, Pos(Succ(wy20800)), wy209, Pos(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup11(wy207, wy20800, wy209, wy21000, wy211, wy212, wy20800, wy21000, ba)
new_lookup17(wy649, wy650, wy651, wy652, Succ(wy6530), Zero, bf) → new_lookup(:%(Pos(Zero), Neg(Succ(wy649))), wy652, bf)
new_lookup15(wy635, wy636, wy637, wy638, Succ(wy6390), Succ(wy6400), bd) → new_lookup15(wy635, wy636, wy637, wy638, wy6390, wy6400, bd)
new_lookup124(wy689, wy690, wy691, wy692, ce) → new_lookup(:%(Neg(Zero), Neg(Succ(wy689))), wy692, ce)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup111(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup14(wy628, wy629, wy630, wy631, Succ(wy6320), Succ(wy6330), bc) → new_lookup14(wy628, wy629, wy630, wy631, wy6320, wy6330, bc)
new_lookup1(wy207, Pos(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, ba)
new_lookup1(wy207, Neg(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, ba)
new_lookup18(wy264, Neg(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, bg)
new_lookup18(wy264, Pos(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, bg)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, Succ(wy7670), Zero, cg) → new_lookup12(wy761, Neg(Succ(wy762)), wy763, Neg(Succ(wy764)), wy765, wy766, cg)
new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, Zero, Succ(wy7680), cg) → new_lookup12(wy761, Neg(Succ(wy762)), wy763, Neg(Succ(wy764)), wy765, wy766, cg)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup110(wy675, wy676, wy677, wy678, Succ(wy6790), Succ(wy6800), cc) → new_lookup110(wy675, wy676, wy677, wy678, wy6790, wy6800, cc)
new_lookup18(wy264, Neg(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, bg)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup111(wy682, wy683, wy684, wy685, Succ(wy6860), Zero, cd) → new_lookup(:%(Neg(Zero), Pos(Succ(wy682))), wy685, cd)
new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, Succ(wy7850), Zero, ca) → new_lookup119(wy779, Neg(Succ(wy780)), wy781, Neg(Succ(wy782)), wy783, wy784, ca)
new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, Zero, Succ(wy7860), ca) → new_lookup119(wy779, Neg(Succ(wy780)), wy781, Neg(Succ(wy782)), wy783, wy784, ca)
new_lookup(:%(Pos(Succ(wy3000)), wy31), :(@2(:%(Pos(Zero), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Succ(wy3000)), wy31), wy41, bb)
new_lookup(:%(Pos(Succ(wy3000)), wy31), :(@2(:%(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup1(wy3000, wy31, wy400000, wy4001, wy401, wy41, wy3000, wy400000, bb)
new_lookup18(wy264, Pos(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, bg)
new_lookup112(wy689, wy690, wy691, wy692, Succ(wy6930), Succ(wy6940), ce) → new_lookup112(wy689, wy690, wy691, wy692, wy6930, wy6940, ce)
new_lookup113(wy628, wy629, wy630, wy631, bc) → new_lookup(:%(Pos(Zero), Pos(Succ(wy628))), wy631, bc)
new_lookup19(wy668, wy669, wy670, wy671, Succ(wy6720), Zero, cb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy668))), wy671, cb)
new_lookup116(wy649, wy650, wy651, wy652, bf) → new_lookup(:%(Pos(Zero), Neg(Succ(wy649))), wy652, bf)
new_lookup17(wy649, wy650, wy651, wy652, Succ(wy6530), Succ(wy6540), bf) → new_lookup17(wy649, wy650, wy651, wy652, wy6530, wy6540, bf)
new_lookup1(wy207, Neg(Succ(wy20800)), wy209, Neg(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup13(wy207, wy20800, wy209, wy21000, wy211, wy212, wy20800, wy21000, ba)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup15(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup114(wy635, wy636, wy637, wy638, bd) → new_lookup(:%(Pos(Zero), Neg(Succ(wy635))), wy638, bd)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup112(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup110(wy675, wy676, wy677, wy678, Zero, Succ(wy6800), cc) → new_lookup122(wy675, wy676, wy677, wy678, cc)
new_lookup(:%(Pos(Zero), wy31), :(@2(:%(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), wy31), wy41, bb)
new_lookup121(wy668, wy669, wy670, wy671, cb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy668))), wy671, cb)
new_lookup115(wy642, wy643, wy644, wy645, be) → new_lookup(:%(Pos(Zero), Pos(Succ(wy642))), wy645, be)
new_lookup12(wy207, wy208, wy209, wy210, wy211, wy212, ba) → new_lookup(:%(Pos(Succ(wy207)), wy208), wy212, ba)
new_lookup1(wy207, Neg(Succ(wy20800)), wy209, Neg(Zero), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Succ(wy20800)), wy209, Neg(Zero), wy211, wy212, ba)
new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, Succ(wy2130), Zero, ba) → new_lookup(:%(Pos(Succ(wy207)), wy208), wy212, ba)
new_lookup14(wy628, wy629, wy630, wy631, Succ(wy6320), Zero, bc) → new_lookup(:%(Pos(Zero), Pos(Succ(wy628))), wy631, bc)
new_lookup18(wy264, Pos(Succ(wy26500)), wy266, Neg(wy2670), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Succ(wy26500)), wy266, Neg(wy2670), wy268, wy269, bg)
new_lookup18(wy264, Neg(Succ(wy26500)), wy266, Pos(wy2670), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Succ(wy26500)), wy266, Pos(wy2670), wy268, wy269, bg)
new_lookup119(wy264, wy265, wy266, wy267, wy268, wy269, bg) → new_lookup(:%(Neg(Succ(wy264)), wy265), wy269, bg)
new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, Zero, Succ(wy7590), cf) → new_lookup12(wy752, Pos(Succ(wy753)), wy754, Pos(Succ(wy755)), wy756, wy757, cf)
new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, Succ(wy7580), Zero, cf) → new_lookup12(wy752, Pos(Succ(wy753)), wy754, Pos(Succ(wy755)), wy756, wy757, cf)
new_lookup10(wy207, wy208, wy209, wy210, wy211, wy212, ba) → new_lookup(:%(Pos(Succ(wy207)), wy208), wy212, ba)
new_lookup111(wy682, wy683, wy684, wy685, Zero, Succ(wy6870), cd) → new_lookup123(wy682, wy683, wy684, wy685, cd)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup16(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Neg(Zero), wy31), :(@2(:%(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), wy31), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup122(wy675, wy676, wy677, wy678, cc) → new_lookup(:%(Neg(Zero), Neg(Succ(wy675))), wy678, cc)
new_lookup18(wy264, Pos(Succ(wy26500)), wy266, Pos(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup118(wy264, wy26500, wy266, wy26700, wy268, wy269, wy26500, wy26700, bg)
new_lookup(:%(Neg(Zero), wy31), :(@2(:%(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), wy31), wy41, bb)
new_lookup112(wy689, wy690, wy691, wy692, Zero, Succ(wy6940), ce) → new_lookup124(wy689, wy690, wy691, wy692, ce)
new_lookup110(wy675, wy676, wy677, wy678, Succ(wy6790), Zero, cc) → new_lookup(:%(Neg(Zero), Neg(Succ(wy675))), wy678, cc)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup1(wy207, Neg(Succ(wy20800)), wy209, Pos(wy2100), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Succ(wy20800)), wy209, Pos(wy2100), wy211, wy212, ba)
new_lookup1(wy207, Pos(Succ(wy20800)), wy209, Neg(wy2100), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Succ(wy20800)), wy209, Neg(wy2100), wy211, wy212, ba)
new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, Succ(wy7670), Succ(wy7680), cg) → new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, wy7670, wy7680, cg)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, Succ(wy2700), Succ(wy2710), bg) → new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, wy2700, wy2710, bg)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup15(wy635, wy636, wy637, wy638, Zero, Succ(wy6400), bd) → new_lookup114(wy635, wy636, wy637, wy638, bd)
new_lookup14(wy628, wy629, wy630, wy631, Zero, Succ(wy6330), bc) → new_lookup113(wy628, wy629, wy630, wy631, bc)
new_lookup1(wy207, Pos(Succ(wy20800)), wy209, Pos(Zero), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Succ(wy20800)), wy209, Pos(Zero), wy211, wy212, ba)
new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, Succ(wy2130), Succ(wy2140), ba) → new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, wy2130, wy2140, ba)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup14(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup18(wy264, Pos(Succ(wy26500)), wy266, Pos(Zero), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Succ(wy26500)), wy266, Pos(Zero), wy268, wy269, bg)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, Succ(wy7850), Succ(wy7860), ca) → new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, wy7850, wy7860, ca)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup19(wy668, wy669, wy670, wy671, Succ(wy6720), Succ(wy6730), cb) → new_lookup19(wy668, wy669, wy670, wy671, wy6720, wy6730, cb)
new_lookup111(wy682, wy683, wy684, wy685, Succ(wy6860), Succ(wy6870), cd) → new_lookup111(wy682, wy683, wy684, wy685, wy6860, wy6870, cd)
new_lookup16(wy642, wy643, wy644, wy645, Succ(wy6460), Succ(wy6470), be) → new_lookup16(wy642, wy643, wy644, wy645, wy6460, wy6470, be)
new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, Zero, Succ(wy2710), bg) → new_lookup117(wy264, wy265, wy266, wy267, wy268, wy269, bg)
new_lookup(:%(Pos(Succ(wy3000)), wy31), :(@2(:%(Neg(wy40000), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Succ(wy3000)), wy31), wy41, bb)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, Succ(wy2700), Zero, bg) → new_lookup(:%(Neg(Succ(wy264)), wy265), wy269, bg)
new_lookup16(wy642, wy643, wy644, wy645, Zero, Succ(wy6470), be) → new_lookup115(wy642, wy643, wy644, wy645, be)
new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, Succ(wy7760), Zero, bh) → new_lookup119(wy770, Pos(Succ(wy771)), wy772, Pos(Succ(wy773)), wy774, wy775, bh)
new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, Zero, Succ(wy7770), bh) → new_lookup119(wy770, Pos(Succ(wy771)), wy772, Pos(Succ(wy773)), wy774, wy775, bh)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup110(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup19(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Neg(Succ(wy3000)), wy31), :(@2(:%(Pos(wy40000), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Succ(wy3000)), wy31), wy41, bb)
new_lookup112(wy689, wy690, wy691, wy692, Succ(wy6930), Zero, ce) → new_lookup(:%(Neg(Zero), Neg(Succ(wy689))), wy692, ce)
new_lookup17(wy649, wy650, wy651, wy652, Zero, Succ(wy6540), bf) → new_lookup116(wy649, wy650, wy651, wy652, bf)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup117(wy264, wy265, wy266, wy267, wy268, wy269, bg) → new_lookup(:%(Neg(Succ(wy264)), wy265), wy269, bg)
new_lookup18(wy264, Neg(Succ(wy26500)), wy266, Neg(Zero), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Succ(wy26500)), wy266, Neg(Zero), wy268, wy269, bg)
new_lookup18(wy264, Pos(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, bg)
new_lookup18(wy264, Neg(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, bg)
new_lookup(:%(Neg(Succ(wy3000)), wy31), :(@2(:%(Neg(Zero), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Succ(wy3000)), wy31), wy41, bb)
new_lookup18(wy264, Neg(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Zero), wy266, Neg(Succ(wy26700)), wy268, wy269, bg)
new_lookup18(wy264, Pos(Succ(wy26500)), wy266, Pos(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup118(wy264, wy26500, wy266, wy26700, wy268, wy269, wy26500, wy26700, bg)
new_lookup18(wy264, Pos(Succ(wy26500)), wy266, Neg(wy2670), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Succ(wy26500)), wy266, Neg(wy2670), wy268, wy269, bg)
new_lookup18(wy264, Neg(Succ(wy26500)), wy266, Pos(wy2670), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Neg(Succ(wy26500)), wy266, Pos(wy2670), wy268, wy269, bg)
new_lookup18(wy264, Neg(Succ(wy26500)), wy266, Neg(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup120(wy264, wy26500, wy266, wy26700, wy268, wy269, wy26500, wy26700, bg)
new_lookup119(wy264, wy265, wy266, wy267, wy268, wy269, bg) → new_lookup(:%(Neg(Succ(wy264)), wy265), wy269, bg)
new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, Succ(wy2700), Zero, bg) → new_lookup(:%(Neg(Succ(wy264)), wy265), wy269, bg)
new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, Succ(wy7760), Zero, bh) → new_lookup119(wy770, Pos(Succ(wy771)), wy772, Pos(Succ(wy773)), wy774, wy775, bh)
new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, Zero, Succ(wy7770), bh) → new_lookup119(wy770, Pos(Succ(wy771)), wy772, Pos(Succ(wy773)), wy774, wy775, bh)
new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, Zero, Succ(wy7860), ca) → new_lookup119(wy779, Neg(Succ(wy780)), wy781, Neg(Succ(wy782)), wy783, wy784, ca)
new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, Succ(wy7850), Zero, ca) → new_lookup119(wy779, Neg(Succ(wy780)), wy781, Neg(Succ(wy782)), wy783, wy784, ca)
new_lookup18(wy264, Pos(Succ(wy26500)), wy266, Pos(Zero), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Succ(wy26500)), wy266, Pos(Zero), wy268, wy269, bg)
new_lookup(:%(Neg(Succ(wy3000)), wy31), :(@2(:%(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup18(wy3000, wy31, wy400000, wy4001, wy401, wy41, wy3000, wy400000, bb)
new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, Succ(wy7850), Succ(wy7860), ca) → new_lookup120(wy779, wy780, wy781, wy782, wy783, wy784, wy7850, wy7860, ca)
new_lookup(:%(Neg(Succ(wy3000)), wy31), :(@2(:%(Pos(wy40000), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Succ(wy3000)), wy31), wy41, bb)
new_lookup18(wy264, Pos(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, Zero, Zero, bg) → new_lookup119(wy264, Pos(Zero), wy266, Pos(Succ(wy26700)), wy268, wy269, bg)
new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, Succ(wy7760), Succ(wy7770), bh) → new_lookup118(wy770, wy771, wy772, wy773, wy774, wy775, wy7760, wy7770, bh)
new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, Zero, Succ(wy2710), bg) → new_lookup117(wy264, wy265, wy266, wy267, wy268, wy269, bg)
new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, Succ(wy2700), Succ(wy2710), bg) → new_lookup18(wy264, wy265, wy266, wy267, wy268, wy269, wy2700, wy2710, bg)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup12(wy207, wy208, wy209, wy210, wy211, wy212, ba) → new_lookup(:%(Pos(Succ(wy207)), wy208), wy212, ba)
new_lookup1(wy207, Pos(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, ba)
new_lookup1(wy207, Neg(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, ba)
new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, Succ(wy7670), Zero, cg) → new_lookup12(wy761, Neg(Succ(wy762)), wy763, Neg(Succ(wy764)), wy765, wy766, cg)
new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, Zero, Succ(wy7680), cg) → new_lookup12(wy761, Neg(Succ(wy762)), wy763, Neg(Succ(wy764)), wy765, wy766, cg)
new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, Succ(wy7580), Succ(wy7590), cf) → new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, wy7580, wy7590, cf)
new_lookup1(wy207, Neg(Succ(wy20800)), wy209, Neg(Zero), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Succ(wy20800)), wy209, Neg(Zero), wy211, wy212, ba)
new_lookup1(wy207, Neg(Succ(wy20800)), wy209, Neg(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup13(wy207, wy20800, wy209, wy21000, wy211, wy212, wy20800, wy21000, ba)
new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, Succ(wy2130), Zero, ba) → new_lookup(:%(Pos(Succ(wy207)), wy208), wy212, ba)
new_lookup(:%(Pos(Succ(wy3000)), wy31), :(@2(:%(Neg(wy40000), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Succ(wy3000)), wy31), wy41, bb)
new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, Zero, Succ(wy2140), ba) → new_lookup10(wy207, wy208, wy209, wy210, wy211, wy212, ba)
new_lookup1(wy207, Pos(Succ(wy20800)), wy209, Pos(Zero), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Succ(wy20800)), wy209, Pos(Zero), wy211, wy212, ba)
new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, Succ(wy2130), Succ(wy2140), ba) → new_lookup1(wy207, wy208, wy209, wy210, wy211, wy212, wy2130, wy2140, ba)
new_lookup1(wy207, Pos(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Zero), wy209, Pos(Succ(wy21000)), wy211, wy212, ba)
new_lookup1(wy207, Pos(Succ(wy20800)), wy209, Pos(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup11(wy207, wy20800, wy209, wy21000, wy211, wy212, wy20800, wy21000, ba)
new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, Zero, Succ(wy7590), cf) → new_lookup12(wy752, Pos(Succ(wy753)), wy754, Pos(Succ(wy755)), wy756, wy757, cf)
new_lookup11(wy752, wy753, wy754, wy755, wy756, wy757, Succ(wy7580), Zero, cf) → new_lookup12(wy752, Pos(Succ(wy753)), wy754, Pos(Succ(wy755)), wy756, wy757, cf)
new_lookup1(wy207, Neg(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Zero), wy209, Neg(Succ(wy21000)), wy211, wy212, ba)
new_lookup(:%(Pos(Succ(wy3000)), wy31), :(@2(:%(Pos(Zero), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Succ(wy3000)), wy31), wy41, bb)
new_lookup10(wy207, wy208, wy209, wy210, wy211, wy212, ba) → new_lookup(:%(Pos(Succ(wy207)), wy208), wy212, ba)
new_lookup1(wy207, Pos(Succ(wy20800)), wy209, Neg(wy2100), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Pos(Succ(wy20800)), wy209, Neg(wy2100), wy211, wy212, ba)
new_lookup1(wy207, Neg(Succ(wy20800)), wy209, Pos(wy2100), wy211, wy212, Zero, Zero, ba) → new_lookup12(wy207, Neg(Succ(wy20800)), wy209, Pos(wy2100), wy211, wy212, ba)
new_lookup(:%(Pos(Succ(wy3000)), wy31), :(@2(:%(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup1(wy3000, wy31, wy400000, wy4001, wy401, wy41, wy3000, wy400000, bb)
new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, Succ(wy7670), Succ(wy7680), cg) → new_lookup13(wy761, wy762, wy763, wy764, wy765, wy766, wy7670, wy7680, cg)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup123(wy682, wy683, wy684, wy685, cd) → new_lookup(:%(Neg(Zero), Pos(Succ(wy682))), wy685, cd)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup110(wy675, wy676, wy677, wy678, Succ(wy6790), Succ(wy6800), cc) → new_lookup110(wy675, wy676, wy677, wy678, wy6790, wy6800, cc)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup111(wy682, wy683, wy684, wy685, Succ(wy6860), Zero, cd) → new_lookup(:%(Neg(Zero), Pos(Succ(wy682))), wy685, cd)
new_lookup19(wy668, wy669, wy670, wy671, Zero, Succ(wy6730), cb) → new_lookup121(wy668, wy669, wy670, wy671, cb)
new_lookup19(wy668, wy669, wy670, wy671, Succ(wy6720), Succ(wy6730), cb) → new_lookup19(wy668, wy669, wy670, wy671, wy6720, wy6730, cb)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup111(wy682, wy683, wy684, wy685, Succ(wy6860), Succ(wy6870), cd) → new_lookup111(wy682, wy683, wy684, wy685, wy6860, wy6870, cd)
new_lookup112(wy689, wy690, wy691, wy692, Succ(wy6930), Succ(wy6940), ce) → new_lookup112(wy689, wy690, wy691, wy692, wy6930, wy6940, ce)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup111(wy682, wy683, wy684, wy685, Zero, Succ(wy6870), cd) → new_lookup123(wy682, wy683, wy684, wy685, cd)
new_lookup19(wy668, wy669, wy670, wy671, Succ(wy6720), Zero, cb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy668))), wy671, cb)
new_lookup(:%(Neg(Zero), wy31), :(@2(:%(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), wy31), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup122(wy675, wy676, wy677, wy678, cc) → new_lookup(:%(Neg(Zero), Neg(Succ(wy675))), wy678, cc)
new_lookup(:%(Neg(Zero), wy31), :(@2(:%(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), wy31), wy41, bb)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup112(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup112(wy689, wy690, wy691, wy692, Zero, Succ(wy6940), ce) → new_lookup124(wy689, wy690, wy691, wy692, ce)
new_lookup(:%(Neg(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup110(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup110(wy675, wy676, wy677, wy678, Succ(wy6790), Zero, cc) → new_lookup(:%(Neg(Zero), Neg(Succ(wy675))), wy678, cc)
new_lookup110(wy675, wy676, wy677, wy678, Zero, Succ(wy6800), cc) → new_lookup122(wy675, wy676, wy677, wy678, cc)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup19(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)
new_lookup121(wy668, wy669, wy670, wy671, cb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy668))), wy671, cb)
new_lookup124(wy689, wy690, wy691, wy692, ce) → new_lookup(:%(Neg(Zero), Neg(Succ(wy689))), wy692, ce)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Neg(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup111(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup112(wy689, wy690, wy691, wy692, Succ(wy6930), Zero, ce) → new_lookup(:%(Neg(Zero), Neg(Succ(wy689))), wy692, ce)
new_lookup(:%(Neg(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Neg(Zero), Pos(Zero)), wy41, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup17(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup14(wy628, wy629, wy630, wy631, Succ(wy6320), Succ(wy6330), bc) → new_lookup14(wy628, wy629, wy630, wy631, wy6320, wy6330, bc)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup15(wy635, wy636, wy637, wy638, Zero, Succ(wy6400), bd) → new_lookup114(wy635, wy636, wy637, wy638, bd)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup14(wy628, wy629, wy630, wy631, Zero, Succ(wy6330), bc) → new_lookup113(wy628, wy629, wy630, wy631, bc)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup14(wy628, wy629, wy630, wy631, Succ(wy6320), Zero, bc) → new_lookup(:%(Pos(Zero), Pos(Succ(wy628))), wy631, bc)
new_lookup16(wy642, wy643, wy644, wy645, Succ(wy6460), Zero, be) → new_lookup(:%(Pos(Zero), Pos(Succ(wy642))), wy645, be)
new_lookup(:%(Pos(Zero), wy31), :(@2(:%(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), wy31), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup14(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Neg(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup15(wy635, wy636, wy637, wy638, Succ(wy6390), Zero, bd) → new_lookup(:%(Pos(Zero), Neg(Succ(wy635))), wy638, bd)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup16(wy642, wy643, wy644, wy645, Succ(wy6460), Succ(wy6470), be) → new_lookup16(wy642, wy643, wy644, wy645, wy6460, wy6470, be)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(wy40010)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), wy41, bb)
new_lookup113(wy628, wy629, wy630, wy631, bc) → new_lookup(:%(Pos(Zero), Pos(Succ(wy628))), wy631, bc)
new_lookup116(wy649, wy650, wy651, wy652, bf) → new_lookup(:%(Pos(Zero), Neg(Succ(wy649))), wy652, bf)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup16(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup17(wy649, wy650, wy651, wy652, Succ(wy6530), Succ(wy6540), bf) → new_lookup17(wy649, wy650, wy651, wy652, wy6530, wy6540, bf)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Succ(wy3100))), :(@2(:%(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup15(wy3100, wy400100, wy401, wy41, wy3100, wy400100, bb)
new_lookup114(wy635, wy636, wy637, wy638, bd) → new_lookup(:%(Pos(Zero), Neg(Succ(wy635))), wy638, bd)
new_lookup16(wy642, wy643, wy644, wy645, Zero, Succ(wy6470), be) → new_lookup115(wy642, wy643, wy644, wy645, be)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Neg(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup17(wy649, wy650, wy651, wy652, Succ(wy6530), Zero, bf) → new_lookup(:%(Pos(Zero), Neg(Succ(wy649))), wy652, bf)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup(:%(Pos(Zero), wy31), :(@2(:%(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), wy31), wy41, bb)
new_lookup15(wy635, wy636, wy637, wy638, Succ(wy6390), Succ(wy6400), bd) → new_lookup15(wy635, wy636, wy637, wy638, wy6390, wy6400, bd)
new_lookup(:%(Pos(Zero), Pos(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Zero)), wy41, bb)
new_lookup115(wy642, wy643, wy644, wy645, be) → new_lookup(:%(Pos(Zero), Pos(Succ(wy642))), wy645, be)
new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), :(@2(:%(Pos(Zero), Pos(Zero)), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Pos(Succ(wy3100))), wy41, bb)
new_lookup(:%(Pos(Zero), Neg(Zero)), :(@2(:%(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(:%(Pos(Zero), Neg(Zero)), wy41, bb)
new_lookup17(wy649, wy650, wy651, wy652, Zero, Succ(wy6540), bf) → new_lookup116(wy649, wy650, wy651, wy652, bf)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: